Left Termination of the query pattern
factor(g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 84 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 53 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇒, 4 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 PiDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 PiDP
        ↳17 PiDPToQDPProof (⇒, 0 ms)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔, 0 ms)
        ↳20 YES
    ↳21 PiDP
        ↳22 UsableRulesProof (⇔, 0 ms)
        ↳23 PiDP
        ↳24 PiDPToQDPProof (⇒, 0 ms)
        ↳25 QDP
        ↳26 MRRProof (⇔, 47 ms)
        ↳27 QDP
        ↳28 PisEmptyProof (⇔, 0 ms)
        ↳29 YES
    ↳30 PiDP
        ↳31 PiDPToQDPProof (⇒, 0 ms)
        ↳32 QDP
        ↳33 QDPOrderProof (⇔, 44 ms)
        ↳34 QDP
        ↳35 DependencyGraphProof (⇔, 2 ms)
        ↳36 TRUE

(0) Obligation:

Clauses:

factor(cons(X, nil), X).
factor(cons(X, cons(Y, Xs)), T) :- ','(times(X, Y, Z), factor(cons(Z, Xs), T)).
times(0, X_, 0).
times(s(X), Y, Z) :- ','(times(X, Y, XY), plus(XY, Y, Z)).
plus(0, X, X).
plus(s(X), Y, s(Z)) :- plus(X, Y, Z).

Query: factor(g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

timesB(s(X1), X2, X3) :- timesB(X1, X2, X4).
timesB(s(X1), X2, X3) :- ','(timescB(X1, X2, X4), plusC(X4, X2, X3)).
plusC(s(X1), X2, s(X3)) :- plusC(X1, X2, X3).
factorA(cons(0, cons(X1, X2)), X3) :- factorA(cons(0, X2), X3).
factorA(cons(s(X1), cons(X2, X3)), X4) :- timesB(X1, X2, X5).
factorA(cons(s(X1), cons(X2, X3)), X4) :- ','(timescB(X1, X2, X5), plusC(X5, X2, X6)).
factorA(cons(s(X1), cons(X2, X3)), X4) :- ','(timescB(X1, X2, X5), ','(pluscC(X5, X2, X6), factorA(cons(X6, X3), X4))).

Clauses:

factorcA(cons(X1, nil), X1).
factorcA(cons(0, cons(X1, X2)), X3) :- factorcA(cons(0, X2), X3).
factorcA(cons(s(X1), cons(X2, X3)), X4) :- ','(timescB(X1, X2, X5), ','(pluscC(X5, X2, X6), factorcA(cons(X6, X3), X4))).
timescB(0, X1, 0).
timescB(s(X1), X2, X3) :- ','(timescB(X1, X2, X4), pluscC(X4, X2, X3)).
pluscC(0, X1, X1).
pluscC(s(X1), X2, s(X3)) :- pluscC(X1, X2, X3).

Afs:

factorA(x1, x2)  =  factorA(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
factorA_in: (b,f)
timesB_in: (b,b,f)
timescB_in: (b,b,f)
pluscC_in: (b,b,f)
plusC_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

FACTORA_IN_GA(cons(0, cons(X1, X2)), X3) → U5_GA(X1, X2, X3, factorA_in_ga(cons(0, X2), X3))
FACTORA_IN_GA(cons(0, cons(X1, X2)), X3) → FACTORA_IN_GA(cons(0, X2), X3)
FACTORA_IN_GA(cons(s(X1), cons(X2, X3)), X4) → U6_GA(X1, X2, X3, X4, timesB_in_gga(X1, X2, X5))
FACTORA_IN_GA(cons(s(X1), cons(X2, X3)), X4) → TIMESB_IN_GGA(X1, X2, X5)
TIMESB_IN_GGA(s(X1), X2, X3) → U1_GGA(X1, X2, X3, timesB_in_gga(X1, X2, X4))
TIMESB_IN_GGA(s(X1), X2, X3) → TIMESB_IN_GGA(X1, X2, X4)
TIMESB_IN_GGA(s(X1), X2, X3) → U2_GGA(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U2_GGA(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U3_GGA(X1, X2, X3, plusC_in_gga(X4, X2, X3))
U2_GGA(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → PLUSC_IN_GGA(X4, X2, X3)
PLUSC_IN_GGA(s(X1), X2, s(X3)) → U4_GGA(X1, X2, X3, plusC_in_gga(X1, X2, X3))
PLUSC_IN_GGA(s(X1), X2, s(X3)) → PLUSC_IN_GGA(X1, X2, X3)
FACTORA_IN_GA(cons(s(X1), cons(X2, X3)), X4) → U7_GA(X1, X2, X3, X4, timescB_in_gga(X1, X2, X5))
U7_GA(X1, X2, X3, X4, timescB_out_gga(X1, X2, X5)) → U8_GA(X1, X2, X3, X4, plusC_in_gga(X5, X2, X6))
U7_GA(X1, X2, X3, X4, timescB_out_gga(X1, X2, X5)) → PLUSC_IN_GGA(X5, X2, X6)
U7_GA(X1, X2, X3, X4, timescB_out_gga(X1, X2, X5)) → U9_GA(X1, X2, X3, X4, pluscC_in_gga(X5, X2, X6))
U9_GA(X1, X2, X3, X4, pluscC_out_gga(X5, X2, X6)) → U10_GA(X1, X2, X3, X4, factorA_in_ga(cons(X6, X3), X4))
U9_GA(X1, X2, X3, X4, pluscC_out_gga(X5, X2, X6)) → FACTORA_IN_GA(cons(X6, X3), X4)

The TRS R consists of the following rules:

timescB_in_gga(0, X1, 0) → timescB_out_gga(0, X1, 0)
timescB_in_gga(s(X1), X2, X3) → U16_gga(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U16_gga(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U17_gga(X1, X2, X3, pluscC_in_gga(X4, X2, X3))
pluscC_in_gga(0, X1, X1) → pluscC_out_gga(0, X1, X1)
pluscC_in_gga(s(X1), X2, s(X3)) → U18_gga(X1, X2, X3, pluscC_in_gga(X1, X2, X3))
U18_gga(X1, X2, X3, pluscC_out_gga(X1, X2, X3)) → pluscC_out_gga(s(X1), X2, s(X3))
U17_gga(X1, X2, X3, pluscC_out_gga(X4, X2, X3)) → timescB_out_gga(s(X1), X2, X3)

The argument filtering Pi contains the following mapping:
factorA_in_ga(x1, x2)  =  factorA_in_ga(x1)
cons(x1, x2)  =  cons(x1, x2)
0  =  0
s(x1)  =  s(x1)
timesB_in_gga(x1, x2, x3)  =  timesB_in_gga(x1, x2)
timescB_in_gga(x1, x2, x3)  =  timescB_in_gga(x1, x2)
timescB_out_gga(x1, x2, x3)  =  timescB_out_gga(x1, x2, x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
pluscC_in_gga(x1, x2, x3)  =  pluscC_in_gga(x1, x2)
pluscC_out_gga(x1, x2, x3)  =  pluscC_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
plusC_in_gga(x1, x2, x3)  =  plusC_in_gga(x1, x2)
FACTORA_IN_GA(x1, x2)  =  FACTORA_IN_GA(x1)
U5_GA(x1, x2, x3, x4)  =  U5_GA(x1, x2, x4)
U6_GA(x1, x2, x3, x4, x5)  =  U6_GA(x1, x2, x3, x5)
TIMESB_IN_GGA(x1, x2, x3)  =  TIMESB_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
PLUSC_IN_GGA(x1, x2, x3)  =  PLUSC_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
U7_GA(x1, x2, x3, x4, x5)  =  U7_GA(x1, x2, x3, x5)
U8_GA(x1, x2, x3, x4, x5)  =  U8_GA(x1, x2, x3, x5)
U9_GA(x1, x2, x3, x4, x5)  =  U9_GA(x1, x2, x3, x5)
U10_GA(x1, x2, x3, x4, x5)  =  U10_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FACTORA_IN_GA(cons(0, cons(X1, X2)), X3) → U5_GA(X1, X2, X3, factorA_in_ga(cons(0, X2), X3))
FACTORA_IN_GA(cons(0, cons(X1, X2)), X3) → FACTORA_IN_GA(cons(0, X2), X3)
FACTORA_IN_GA(cons(s(X1), cons(X2, X3)), X4) → U6_GA(X1, X2, X3, X4, timesB_in_gga(X1, X2, X5))
FACTORA_IN_GA(cons(s(X1), cons(X2, X3)), X4) → TIMESB_IN_GGA(X1, X2, X5)
TIMESB_IN_GGA(s(X1), X2, X3) → U1_GGA(X1, X2, X3, timesB_in_gga(X1, X2, X4))
TIMESB_IN_GGA(s(X1), X2, X3) → TIMESB_IN_GGA(X1, X2, X4)
TIMESB_IN_GGA(s(X1), X2, X3) → U2_GGA(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U2_GGA(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U3_GGA(X1, X2, X3, plusC_in_gga(X4, X2, X3))
U2_GGA(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → PLUSC_IN_GGA(X4, X2, X3)
PLUSC_IN_GGA(s(X1), X2, s(X3)) → U4_GGA(X1, X2, X3, plusC_in_gga(X1, X2, X3))
PLUSC_IN_GGA(s(X1), X2, s(X3)) → PLUSC_IN_GGA(X1, X2, X3)
FACTORA_IN_GA(cons(s(X1), cons(X2, X3)), X4) → U7_GA(X1, X2, X3, X4, timescB_in_gga(X1, X2, X5))
U7_GA(X1, X2, X3, X4, timescB_out_gga(X1, X2, X5)) → U8_GA(X1, X2, X3, X4, plusC_in_gga(X5, X2, X6))
U7_GA(X1, X2, X3, X4, timescB_out_gga(X1, X2, X5)) → PLUSC_IN_GGA(X5, X2, X6)
U7_GA(X1, X2, X3, X4, timescB_out_gga(X1, X2, X5)) → U9_GA(X1, X2, X3, X4, pluscC_in_gga(X5, X2, X6))
U9_GA(X1, X2, X3, X4, pluscC_out_gga(X5, X2, X6)) → U10_GA(X1, X2, X3, X4, factorA_in_ga(cons(X6, X3), X4))
U9_GA(X1, X2, X3, X4, pluscC_out_gga(X5, X2, X6)) → FACTORA_IN_GA(cons(X6, X3), X4)

The TRS R consists of the following rules:

timescB_in_gga(0, X1, 0) → timescB_out_gga(0, X1, 0)
timescB_in_gga(s(X1), X2, X3) → U16_gga(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U16_gga(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U17_gga(X1, X2, X3, pluscC_in_gga(X4, X2, X3))
pluscC_in_gga(0, X1, X1) → pluscC_out_gga(0, X1, X1)
pluscC_in_gga(s(X1), X2, s(X3)) → U18_gga(X1, X2, X3, pluscC_in_gga(X1, X2, X3))
U18_gga(X1, X2, X3, pluscC_out_gga(X1, X2, X3)) → pluscC_out_gga(s(X1), X2, s(X3))
U17_gga(X1, X2, X3, pluscC_out_gga(X4, X2, X3)) → timescB_out_gga(s(X1), X2, X3)

The argument filtering Pi contains the following mapping:
factorA_in_ga(x1, x2)  =  factorA_in_ga(x1)
cons(x1, x2)  =  cons(x1, x2)
0  =  0
s(x1)  =  s(x1)
timesB_in_gga(x1, x2, x3)  =  timesB_in_gga(x1, x2)
timescB_in_gga(x1, x2, x3)  =  timescB_in_gga(x1, x2)
timescB_out_gga(x1, x2, x3)  =  timescB_out_gga(x1, x2, x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
pluscC_in_gga(x1, x2, x3)  =  pluscC_in_gga(x1, x2)
pluscC_out_gga(x1, x2, x3)  =  pluscC_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
plusC_in_gga(x1, x2, x3)  =  plusC_in_gga(x1, x2)
FACTORA_IN_GA(x1, x2)  =  FACTORA_IN_GA(x1)
U5_GA(x1, x2, x3, x4)  =  U5_GA(x1, x2, x4)
U6_GA(x1, x2, x3, x4, x5)  =  U6_GA(x1, x2, x3, x5)
TIMESB_IN_GGA(x1, x2, x3)  =  TIMESB_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
PLUSC_IN_GGA(x1, x2, x3)  =  PLUSC_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
U7_GA(x1, x2, x3, x4, x5)  =  U7_GA(x1, x2, x3, x5)
U8_GA(x1, x2, x3, x4, x5)  =  U8_GA(x1, x2, x3, x5)
U9_GA(x1, x2, x3, x4, x5)  =  U9_GA(x1, x2, x3, x5)
U10_GA(x1, x2, x3, x4, x5)  =  U10_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 11 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PLUSC_IN_GGA(s(X1), X2, s(X3)) → PLUSC_IN_GGA(X1, X2, X3)

The TRS R consists of the following rules:

timescB_in_gga(0, X1, 0) → timescB_out_gga(0, X1, 0)
timescB_in_gga(s(X1), X2, X3) → U16_gga(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U16_gga(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U17_gga(X1, X2, X3, pluscC_in_gga(X4, X2, X3))
pluscC_in_gga(0, X1, X1) → pluscC_out_gga(0, X1, X1)
pluscC_in_gga(s(X1), X2, s(X3)) → U18_gga(X1, X2, X3, pluscC_in_gga(X1, X2, X3))
U18_gga(X1, X2, X3, pluscC_out_gga(X1, X2, X3)) → pluscC_out_gga(s(X1), X2, s(X3))
U17_gga(X1, X2, X3, pluscC_out_gga(X4, X2, X3)) → timescB_out_gga(s(X1), X2, X3)

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
timescB_in_gga(x1, x2, x3)  =  timescB_in_gga(x1, x2)
timescB_out_gga(x1, x2, x3)  =  timescB_out_gga(x1, x2, x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
pluscC_in_gga(x1, x2, x3)  =  pluscC_in_gga(x1, x2)
pluscC_out_gga(x1, x2, x3)  =  pluscC_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
PLUSC_IN_GGA(x1, x2, x3)  =  PLUSC_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PLUSC_IN_GGA(s(X1), X2, s(X3)) → PLUSC_IN_GGA(X1, X2, X3)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
PLUSC_IN_GGA(x1, x2, x3)  =  PLUSC_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUSC_IN_GGA(s(X1), X2) → PLUSC_IN_GGA(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • PLUSC_IN_GGA(s(X1), X2) → PLUSC_IN_GGA(X1, X2)
    The graph contains the following edges 1 > 1, 2 >= 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TIMESB_IN_GGA(s(X1), X2, X3) → TIMESB_IN_GGA(X1, X2, X4)

The TRS R consists of the following rules:

timescB_in_gga(0, X1, 0) → timescB_out_gga(0, X1, 0)
timescB_in_gga(s(X1), X2, X3) → U16_gga(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U16_gga(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U17_gga(X1, X2, X3, pluscC_in_gga(X4, X2, X3))
pluscC_in_gga(0, X1, X1) → pluscC_out_gga(0, X1, X1)
pluscC_in_gga(s(X1), X2, s(X3)) → U18_gga(X1, X2, X3, pluscC_in_gga(X1, X2, X3))
U18_gga(X1, X2, X3, pluscC_out_gga(X1, X2, X3)) → pluscC_out_gga(s(X1), X2, s(X3))
U17_gga(X1, X2, X3, pluscC_out_gga(X4, X2, X3)) → timescB_out_gga(s(X1), X2, X3)

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
timescB_in_gga(x1, x2, x3)  =  timescB_in_gga(x1, x2)
timescB_out_gga(x1, x2, x3)  =  timescB_out_gga(x1, x2, x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
pluscC_in_gga(x1, x2, x3)  =  pluscC_in_gga(x1, x2)
pluscC_out_gga(x1, x2, x3)  =  pluscC_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
TIMESB_IN_GGA(x1, x2, x3)  =  TIMESB_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TIMESB_IN_GGA(s(X1), X2, X3) → TIMESB_IN_GGA(X1, X2, X4)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
TIMESB_IN_GGA(x1, x2, x3)  =  TIMESB_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TIMESB_IN_GGA(s(X1), X2) → TIMESB_IN_GGA(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • TIMESB_IN_GGA(s(X1), X2) → TIMESB_IN_GGA(X1, X2)
    The graph contains the following edges 1 > 1, 2 >= 2

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FACTORA_IN_GA(cons(0, cons(X1, X2)), X3) → FACTORA_IN_GA(cons(0, X2), X3)

The TRS R consists of the following rules:

timescB_in_gga(0, X1, 0) → timescB_out_gga(0, X1, 0)
timescB_in_gga(s(X1), X2, X3) → U16_gga(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U16_gga(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U17_gga(X1, X2, X3, pluscC_in_gga(X4, X2, X3))
pluscC_in_gga(0, X1, X1) → pluscC_out_gga(0, X1, X1)
pluscC_in_gga(s(X1), X2, s(X3)) → U18_gga(X1, X2, X3, pluscC_in_gga(X1, X2, X3))
U18_gga(X1, X2, X3, pluscC_out_gga(X1, X2, X3)) → pluscC_out_gga(s(X1), X2, s(X3))
U17_gga(X1, X2, X3, pluscC_out_gga(X4, X2, X3)) → timescB_out_gga(s(X1), X2, X3)

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
0  =  0
s(x1)  =  s(x1)
timescB_in_gga(x1, x2, x3)  =  timescB_in_gga(x1, x2)
timescB_out_gga(x1, x2, x3)  =  timescB_out_gga(x1, x2, x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
pluscC_in_gga(x1, x2, x3)  =  pluscC_in_gga(x1, x2)
pluscC_out_gga(x1, x2, x3)  =  pluscC_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
FACTORA_IN_GA(x1, x2)  =  FACTORA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FACTORA_IN_GA(cons(0, cons(X1, X2)), X3) → FACTORA_IN_GA(cons(0, X2), X3)

R is empty.
The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
0  =  0
FACTORA_IN_GA(x1, x2)  =  FACTORA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FACTORA_IN_GA(cons(0, cons(X1, X2))) → FACTORA_IN_GA(cons(0, X2))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(26) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

FACTORA_IN_GA(cons(0, cons(X1, X2))) → FACTORA_IN_GA(cons(0, X2))


Used ordering: Knuth-Bendix order [KBO] with precedence:
0 > cons2 > FACTORAINGA1

and weight map:

0=1
FACTORA_IN_GA_1=1
cons_2=0

The variable weight is 1

(27) Obligation:

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(28) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(29) YES

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FACTORA_IN_GA(cons(s(X1), cons(X2, X3)), X4) → U7_GA(X1, X2, X3, X4, timescB_in_gga(X1, X2, X5))
U7_GA(X1, X2, X3, X4, timescB_out_gga(X1, X2, X5)) → U9_GA(X1, X2, X3, X4, pluscC_in_gga(X5, X2, X6))
U9_GA(X1, X2, X3, X4, pluscC_out_gga(X5, X2, X6)) → FACTORA_IN_GA(cons(X6, X3), X4)

The TRS R consists of the following rules:

timescB_in_gga(0, X1, 0) → timescB_out_gga(0, X1, 0)
timescB_in_gga(s(X1), X2, X3) → U16_gga(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U16_gga(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U17_gga(X1, X2, X3, pluscC_in_gga(X4, X2, X3))
pluscC_in_gga(0, X1, X1) → pluscC_out_gga(0, X1, X1)
pluscC_in_gga(s(X1), X2, s(X3)) → U18_gga(X1, X2, X3, pluscC_in_gga(X1, X2, X3))
U18_gga(X1, X2, X3, pluscC_out_gga(X1, X2, X3)) → pluscC_out_gga(s(X1), X2, s(X3))
U17_gga(X1, X2, X3, pluscC_out_gga(X4, X2, X3)) → timescB_out_gga(s(X1), X2, X3)

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
0  =  0
s(x1)  =  s(x1)
timescB_in_gga(x1, x2, x3)  =  timescB_in_gga(x1, x2)
timescB_out_gga(x1, x2, x3)  =  timescB_out_gga(x1, x2, x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
pluscC_in_gga(x1, x2, x3)  =  pluscC_in_gga(x1, x2)
pluscC_out_gga(x1, x2, x3)  =  pluscC_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
FACTORA_IN_GA(x1, x2)  =  FACTORA_IN_GA(x1)
U7_GA(x1, x2, x3, x4, x5)  =  U7_GA(x1, x2, x3, x5)
U9_GA(x1, x2, x3, x4, x5)  =  U9_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(31) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FACTORA_IN_GA(cons(s(X1), cons(X2, X3))) → U7_GA(X1, X2, X3, timescB_in_gga(X1, X2))
U7_GA(X1, X2, X3, timescB_out_gga(X1, X2, X5)) → U9_GA(X1, X2, X3, pluscC_in_gga(X5, X2))
U9_GA(X1, X2, X3, pluscC_out_gga(X5, X2, X6)) → FACTORA_IN_GA(cons(X6, X3))

The TRS R consists of the following rules:

timescB_in_gga(0, X1) → timescB_out_gga(0, X1, 0)
timescB_in_gga(s(X1), X2) → U16_gga(X1, X2, timescB_in_gga(X1, X2))
U16_gga(X1, X2, timescB_out_gga(X1, X2, X4)) → U17_gga(X1, X2, pluscC_in_gga(X4, X2))
pluscC_in_gga(0, X1) → pluscC_out_gga(0, X1, X1)
pluscC_in_gga(s(X1), X2) → U18_gga(X1, X2, pluscC_in_gga(X1, X2))
U18_gga(X1, X2, pluscC_out_gga(X1, X2, X3)) → pluscC_out_gga(s(X1), X2, s(X3))
U17_gga(X1, X2, pluscC_out_gga(X4, X2, X3)) → timescB_out_gga(s(X1), X2, X3)

The set Q consists of the following terms:

timescB_in_gga(x0, x1)
U16_gga(x0, x1, x2)
pluscC_in_gga(x0, x1)
U18_gga(x0, x1, x2)
U17_gga(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(33) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


FACTORA_IN_GA(cons(s(X1), cons(X2, X3))) → U7_GA(X1, X2, X3, timescB_in_gga(X1, X2))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(FACTORA_IN_GA(x1)) = x1   
POL(U16_gga(x1, x2, x3)) = 0   
POL(U17_gga(x1, x2, x3)) = 0   
POL(U18_gga(x1, x2, x3)) = 1   
POL(U7_GA(x1, x2, x3, x4)) = 1 + x3   
POL(U9_GA(x1, x2, x3, x4)) = x3 + x4   
POL(cons(x1, x2)) = 1 + x2   
POL(pluscC_in_gga(x1, x2)) = 1   
POL(pluscC_out_gga(x1, x2, x3)) = 1   
POL(s(x1)) = 0   
POL(timescB_in_gga(x1, x2)) = 0   
POL(timescB_out_gga(x1, x2, x3)) = 0   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

pluscC_in_gga(0, X1) → pluscC_out_gga(0, X1, X1)
pluscC_in_gga(s(X1), X2) → U18_gga(X1, X2, pluscC_in_gga(X1, X2))
U18_gga(X1, X2, pluscC_out_gga(X1, X2, X3)) → pluscC_out_gga(s(X1), X2, s(X3))

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U7_GA(X1, X2, X3, timescB_out_gga(X1, X2, X5)) → U9_GA(X1, X2, X3, pluscC_in_gga(X5, X2))
U9_GA(X1, X2, X3, pluscC_out_gga(X5, X2, X6)) → FACTORA_IN_GA(cons(X6, X3))

The TRS R consists of the following rules:

timescB_in_gga(0, X1) → timescB_out_gga(0, X1, 0)
timescB_in_gga(s(X1), X2) → U16_gga(X1, X2, timescB_in_gga(X1, X2))
U16_gga(X1, X2, timescB_out_gga(X1, X2, X4)) → U17_gga(X1, X2, pluscC_in_gga(X4, X2))
pluscC_in_gga(0, X1) → pluscC_out_gga(0, X1, X1)
pluscC_in_gga(s(X1), X2) → U18_gga(X1, X2, pluscC_in_gga(X1, X2))
U18_gga(X1, X2, pluscC_out_gga(X1, X2, X3)) → pluscC_out_gga(s(X1), X2, s(X3))
U17_gga(X1, X2, pluscC_out_gga(X4, X2, X3)) → timescB_out_gga(s(X1), X2, X3)

The set Q consists of the following terms:

timescB_in_gga(x0, x1)
U16_gga(x0, x1, x2)
pluscC_in_gga(x0, x1)
U18_gga(x0, x1, x2)
U17_gga(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(35) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(36) TRUE